g:OMon. (goset)  LOSet 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), GrpSig, Mon, AbMon, gset, OMon, goset
Definitions	x,y. t(x;y), P & Q, , x f y, t  T, x:A. B(x), , t.2, t.1, gset, =, DSet, QOSet, a  b, |p|, POSet{i}, goset, LOSet, Preorder(T;x,y.R(x;y)), Mon, x(s1,s2), AbMon, OMon, Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), IsMonoid(T;op;id)
Lemmas	omon wf, grp eq wf, eqfun p wf, grp id wf, monoid p wf, grp sig wf, mon properties, grp op wf, comm wf, mon wf, abmonoid properties, grp le wf, assert wf, grp car wf, linorder wf, abmonoid wf, omon properties, connex wf, anti sym wf, set leq wf, preorder wf, set eq wf, set car wf, oset of ocmon wf0